Nuprl Lemma : assert_of_band 13,42

p, q:. ((p  q))  ((p) & (q)) 
latex


Upbool 1, bool 1
Definitionst  T, x:A. B(x), , P  Q, P  Q, True, ff, if b then t else f fi , tt, P & Q, p  q, b, P  Q, False, Unit, ,
Lemmasbool wf, false wf, true wf

origin